T:Type, x:T, L, L1, L2:T List. interleaving(T;L1;L2;L)  interleaving(T;x.L1;L2;x.L) 

latex

Definitions

||as||, P  Q, False, A, P & Q, AB, i  j < k, t  T, True, T, , {i..j}, x:A. B(x), Prop, l[i], S  T, S  T, increasing(f;k), x:A. B(x), fshift(f;x), fadd(f;g), ij, disjoint_sublists(T;L1;L2;L), interleaving(T;L1;L2;L), null(as), P  Q, Dec(P), b, P  Q, {T}, SQType(T), nondecreasing(f;k), hd(l), i<j, ij, b, , i=j, Unit, P  Q

Lemmas

length cons, squash wf, select cons tl, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, assert of eq int, eq int wf, bool wf, bnot wf, const nondecreasing, fadd increasing, fshift increasing, not functionality wrt iff, assert wf, non nil length, assert of null, decidable assert, null wf, interleaving wf, fshift wf, fadd wf, non neg length, increasing wf, int seg wf, select wf, not wf, le wf, length wf1